i:Id, l:IdLnk, tg, n, f, k:Top.
msg-spec-loc(k sends on l with tag tg [s,v.f(s,v)], at marker n;i)  source(l) = i 

latex

Definitions	t  T, x:A. B(x), source(l), Id, s = t, IdLnk, Prop, type List, nil, car.cdr, (x  l), x:AB(x), P  Q, x.A(x), P  Q, x:AB(x), P & Q, P  Q, {T}, x. t(x), Void, x:A. B(x), Top, x,y. t(x;y), msg-spec-loc(snd;i), SQType(T), s ~ t
Lemmas	IdLnk sq, top wf, msg-spec-links-spec1, iff functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, member singleton, l member wf, IdLnk wf, Id wf, lsrc wf